A, B:MsgAForm, ltg:(IdLnkIdType), i:Id.
(ltg  ma-outlinks(A  B;i))  (ltg  ma-outlinks(A;i))  (ltg  ma-outlinks(B;i)) 

latex

Definitions	P  Q, da-outlinks(da;i), f  g, x. t(x), Knd, KindDeq, mk-ma, MsgAForm, (x  l), Id, IdLnk, ma-outlinks(M;i), M1  M2, P  Q, x:A. B(x), MsgA, t  T, M1 ||decl M2
Lemmas	ma-join wf, ma-outlinks wf, l member wf, Id wf, IdLnk wf, msg-form wf, da-outlinks-join, Kind-deq wf, Knd wf, fpf-join wf, da-outlinks wf